\cleardoublepage
\begin{vcenterpage}
\noindent\rule[2pt]{\textwidth}{0.5pt}
\begin{center}
{\large\textbf{\eltitulo}\\}
\end{center}
%{\textbf{Abstract}}\\
\emph{Higher-order process calculi} are 
%calculi 
formalisms for concurrency 
in which processes can be passed around in communications.
Higher-order (or process-passing) concurrency is often presented as an alternative paradigm to the first order (or name-passing)
concurrency of the $\pi$-calculus for the description of mobile systems. These calculi are
inspired by, and formally close to, the $\lambda$-calculus, whose basic computational step ---$\beta$-reduction---
involves term instantiation. \\
%This is in opposition to \emph{first-order} calculi, such as CCS and the $\pi$-calculus, 
%in which only basic values (messages) are exchanged.
%As such, higher-order languages thus embody a communication discipline in which exchanged objects can have a complex structure.
%As such, these calculi may provide a convenient framework for
%understanding forms of \emph{code mobility} at a foundational level.\\

%In particular, the higher-order communication paradigm is reminiscent of applications and frameworks exhibiting \emph{code mobility}. \\

The theory of higher-order process calculi is more complex than that of first-order process calculi.
This shows up in, for instance, the definition of behavioral equivalences.
A long-standing approach to overcome this burden is to define
\emph{encodings} of higher-order processes into a first-order setting, so as to 
transfer the 
theory of the first-order paradigm to the 
higher-order one.
%This motivated %led to %a number of \emph{relative} 
%expressiveness studies relating both paradigms: the objective was to alleviate the theoretical burden associated to higher-order languages by appealing to encodings into some first-order setting.
While satisfactory in the case of calculi with basic (higher-order) primitives,
this indirect approach falls short in the case of higher-order process calculi 
featuring  constructs 
%representing specialized 
for 
%emerging  
phenomena %in modern distributed systems 
such as, e.g., %those necessary to represent 
localities and dynamic system reconfiguration, 
which are frequent in modern distributed systems. 
Indeed, for higher-order process calculi involving 
%such constructs, 
little more than traditional process communication, 
encodings into some first-order language are difficult to handle or do not exist. 
%Consequently, f
We then observe that foundational studies for higher-order process calculi 
%(including those related to expressiveness) 
must be carried out \emph{directly} on them and exploit their peculiarities. \\

This dissertation contributes to such foundational studies for higher-order process calculi.
We concentrate on two %intimately 
closely
interwoven issues  in process calculi:
\emph{expressiveness} and \emph{decidability}.
Surprisingly, these issues have been little explored in the higher-order setting.
Our research is centered around a \emph{core} calculus for higher-order 
concurrency in which only the operators strictly necessary to obtain higher-order
communication are retained.
%In addition to 
We 
develop the basic theory of this core calculus and 
rely on it to study
the expressive power of 
%phenomena 
issues
universally accepted as \emph{basic} in process calculi, 
namely synchrony, forwarding, and polyadic communication. \\
%Our results thus bring out novel insights on the nature of higher-order communication and 
%their associated phenomena. \\


\noindent {\textbf{Keywords:}} concurrency theory,  process calculi, higher-order communication, expressiveness, decidability.
\\
\noindent\rule[2pt]{\textwidth}{0.5pt}
 \end{vcenterpage}